Thanks @TashiWalde! Cf. also [BW23, Subsection 3.1.2].

• For every map f : B -> A right orthogonal to ϕ ⊂ ψ, the fibers fib B A f a have unique extensions with respect to ϕ ⊂ ψ.
• As a corollary we get that for any map between types with unique extensions, the fibers have again unique extensions.
• In particular, this answers a question I was discussing with @emilyriehl : every map between Segal types has Segal fibers. I haven't yet formalized that specific instance, since I wasn't sure if this was something someone else (@nimarasekh ?) already did/wanted to do.
• I have also reorganized and expanded the material about functoriality of extension types in 03-extension-types.

Just to make sure, I don't think I had any particular plans to formalize this statement, as I was working on other stuff in Section 8 (whereas to me this seems like it would fit into Section 5)? So @TashiWalde you should feel free to go for it if you want.